(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_IDL)
(declare-fun v0 () Int)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(declare-fun v3 () Int)
(declare-fun v4 () Int)
(declare-fun v5 () Int)
(assert (let ((e6 3044))
(let ((e7 717307937888699))
(let ((e8 1))
(let ((e9 532995695784405))
(let ((e10 139358193))
(let ((e11 77363600))
(let ((e12 (< (- v1 v4) e11)))
(let ((e13 (>= v4 v0)))
(let ((e14 (< v0 v0)))
(let ((e15 (= (- v1 v5) (- e6))))
(let ((e16 (< (- v0 v1) e6)))
(let ((e17 (<= (- v3 v1) e6)))
(let ((e18 (<= (- v1 v3) (- e6))))
(let ((e19 (= v1 v2)))
(let ((e20 (> (- v4 v4) (- e9))))
(let ((e21 (= v0 v1)))
(let ((e22 (> (- v1 v1) (- e7))))
(let ((e23 (<= (- v2 v0) (- e7))))
(let ((e24 (<= (- v1 v5) (- e7))))
(let ((e25 (<= v1 v2)))
(let ((e26 (> (- v1 v2) (- e7))))
(let ((e27 (< v3 v1)))
(let ((e28 (> (- v1 v3) e11)))
(let ((e29 (< (- v0 v3) e9)))
(let ((e30 (<= v2 v3)))
(let ((e31 (>= (- v4 v1) e11)))
(let ((e32 (= (- v3 v1) e11)))
(let ((e33 (distinct v2 v4)))
(let ((e34 (distinct v4 v2)))
(let ((e35 (distinct v4 v4)))
(let ((e36 (>= v3 v2)))
(let ((e37 (> v5 v5)))
(let ((e38 (> v2 v3)))
(let ((e39 (> v5 v5)))
(let ((e40 (= (- v4 v1) (- e9))))
(let ((e41 (< (- v1 v5) e10)))
(let ((e42 (= (- v0 v4) e8)))
(let ((e43 (<= (- v5 v3) e7)))
(let ((e44 (distinct v2 v4)))
(let ((e45 (= v1 v1)))
(let ((e46 (= (- v3 v4) e6)))
(let ((e47 (>= v0 v0)))
(let ((e48 (distinct v1 v2)))
(let ((e49 (< v3 v2)))
(let ((e50 (> v2 v4)))
(let ((e51 (distinct (- v1 v0) e6)))
(let ((e52 (<= v0 v1)))
(let ((e53 (distinct v2 v5)))
(let ((e54 (distinct (- v4 v1) e7)))
(let ((e55 (< v2 v4)))
(let ((e56 (>= v2 v2)))
(let ((e57 (distinct (- v0 v4) e7)))
(let ((e58 (= v0 v1)))
(let ((e59 (>= v4 v3)))
(let ((e60 (distinct (- v2 v2) (- e9))))
(let ((e61 (> v5 v1)))
(let ((e62 (distinct (- v2 v2) (- e8))))
(let ((e63 (distinct (- v1 v1) e6)))
(let ((e64 (= (- v4 v0) e6)))
(let ((e65 (distinct (- v1 v0) (- e7))))
(let ((e66 (= (- v0 v3) (- e6))))
(let ((e67 (distinct (- v2 v5) (- e11))))
(let ((e68 (<= (- v4 v2) (- e11))))
(let ((e69 (>= (- v3 v5) (- e7))))
(let ((e70 (< (- v5 v2) (- e9))))
(let ((e71 (= (- v1 v1) e10)))
(let ((e72 (distinct (- v1 v1) e9)))
(let ((e73 (< v4 v4)))
(let ((e74 (< v0 v0)))
(let ((e75 (ite e24 e56 e67)))
(let ((e76 (not e48)))
(let ((e77 (=> e18 e49)))
(let ((e78 (= e12 e64)))
(let ((e79 (ite e75 e63 e14)))
(let ((e80 (ite e57 e55 e72)))
(let ((e81 (ite e36 e60 e59)))
(let ((e82 (and e20 e69)))
(let ((e83 (xor e73 e41)))
(let ((e84 (xor e13 e68)))
(let ((e85 (= e61 e35)))
(let ((e86 (ite e82 e46 e53)))
(let ((e87 (ite e44 e83 e38)))
(let ((e88 (xor e40 e26)))
(let ((e89 (ite e47 e27 e54)))
(let ((e90 (= e51 e58)))
(let ((e91 (= e85 e77)))
(let ((e92 (not e30)))
(let ((e93 (ite e42 e79 e79)))
(let ((e94 (xor e50 e45)))
(let ((e95 (and e25 e16)))
(let ((e96 (xor e29 e17)))
(let ((e97 (= e71 e80)))
(let ((e98 (xor e32 e65)))
(let ((e99 (ite e96 e70 e34)))
(let ((e100 (xor e39 e28)))
(let ((e101 (and e100 e86)))
(let ((e102 (not e97)))
(let ((e103 (xor e93 e43)))
(let ((e104 (ite e90 e19 e84)))
(let ((e105 (or e92 e23)))
(let ((e106 (= e103 e94)))
(let ((e107 (= e105 e99)))
(let ((e108 (not e37)))
(let ((e109 (=> e102 e104)))
(let ((e110 (or e31 e76)))
(let ((e111 (or e110 e101)))
(let ((e112 (= e52 e88)))
(let ((e113 (or e108 e107)))
(let ((e114 (=> e98 e78)))
(let ((e115 (=> e113 e106)))
(let ((e116 (=> e111 e66)))
(let ((e117 (= e95 e112)))
(let ((e118 (not e117)))
(let ((e119 (xor e33 e89)))
(let ((e120 (=> e74 e116)))
(let ((e121 (not e119)))
(let ((e122 (or e114 e87)))
(let ((e123 (and e122 e21)))
(let ((e124 (and e120 e22)))
(let ((e125 (and e62 e124)))
(let ((e126 (xor e81 e81)))
(let ((e127 (=> e91 e121)))
(let ((e128 (= e118 e115)))
(let ((e129 (and e127 e109)))
(let ((e130 (= e128 e128)))
(let ((e131 (or e130 e126)))
(let ((e132 (and e15 e125)))
(let ((e133 (and e123 e131)))
(let ((e134 (and e133 e132)))
(let ((e135 (=> e129 e129)))
(let ((e136 (or e134 e134)))
(let ((e137 (and e135 e136)))
e137
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
